perm filename BACKUP.TMP[F78,JMC] blob
sn#390440 filedate 1978-10-21 generic text, type T, neo UTF8
show proof 25:↑;
rewrite 2: by FOO ∪ {29 28};
CANCEL;
CANCEL;
∀E LESS4 z x y;
cancel;
∀e LESS4 z pred x y;
cancel;
∀e LESS4 pred x z y;
∀e LESS5 z y;
taut ¬(pred x ≤ z) 33 34 19 29;
rewrite 2: by FOO ∪{28 29 35};
rewrite 2: by FOO ∪{29 30};
⊃I 28 31;
⊃I 30 32;
TAUT 2: 38 39;
⊃I 28 36;
⊃I 30 37;
TAUT 2: 41 42;
⊃I 27 40;
⊃I 29 43;
TAUT 2: 44 45;
⊃I 18 46;
SHOW PROOF 17;
TAUT 2: 17 47;
⊃I 4 48;
TAUT 2: 3 49;
SHOW PROOF → TAK2.PRF;
EXIT;